YES 1.762 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/empty.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:



HASKELL
  ↳ BR

mainModule Main
  ((lookup :: (Eq a, Eq b) => (b,a ->  [((b,a),c)]  ->  Maybe c) :: (Eq b, Eq a) => (b,a ->  [((b,a),c)]  ->  Maybe c)

module Main where
  import qualified Prelude



Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL
  ↳ BR
HASKELL
      ↳ COR

mainModule Main
  ((lookup :: (Eq c, Eq a) => (c,a ->  [((c,a),b)]  ->  Maybe b) :: (Eq c, Eq a) => (c,a ->  [((c,a),b)]  ->  Maybe b)

module Main where
  import qualified Prelude



Cond Reductions:
The following Function with conditions
undefined 
 | False
 = undefined

is transformed to
undefined  = undefined1

undefined0 True = undefined

undefined1  = undefined0 False

The following Function with conditions
lookup k [] = Nothing
lookup k ((x,y: xys)
 | k == x
 = Just y
 | otherwise
 = lookup k xys

is transformed to
lookup k [] = lookup3 k []
lookup k ((x,y: xys) = lookup2 k ((x,y: xys)

lookup0 k x y xys True = lookup k xys

lookup1 k x y xys True = Just y
lookup1 k x y xys False = lookup0 k x y xys otherwise

lookup2 k ((x,y: xys) = lookup1 k x y xys (k == x)

lookup3 k [] = Nothing
lookup3 xy xz = lookup2 xy xz



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
HASKELL
          ↳ Narrow

mainModule Main
  (lookup :: (Eq a, Eq c) => (a,c ->  [((a,c),b)]  ->  Maybe b)

module Main where
  import qualified Prelude



Haskell To QDPs


↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
QDP
                ↳ QDPSizeChangeProof
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primPlusNat(Succ(yu4800), Succ(yu40011000)) → new_primPlusNat(yu4800, yu40011000)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
              ↳ QDP
QDP
                ↳ QDPSizeChangeProof
              ↳ QDP
              ↳ QDP
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primMulNat(Succ(yu31100), Succ(yu4001100)) → new_primMulNat(yu31100, Succ(yu4001100))

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
              ↳ QDP
              ↳ QDP
QDP
                ↳ QDPSizeChangeProof
              ↳ QDP
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primEqNat(Succ(yu3100), Succ(yu400100)) → new_primEqNat(yu3100, yu400100)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
QDP
                ↳ QDPSizeChangeProof
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_esEs(@2(yu310, yu311), @2(yu40010, yu40011), app(app(ty_@2, cc), cd), ce) → new_esEs(yu310, yu40010, cc, cd)
new_esEs2(@3(yu310, yu311, yu312), @3(yu40010, yu40011, yu40012), app(app(app(ty_@3, bcg), bch), bda), hf, bbb) → new_esEs2(yu310, yu40010, bcg, bch, bda)
new_esEs1(:(yu310, yu311), :(yu40010, yu40011), app(app(ty_@2, gd), ge)) → new_esEs(yu310, yu40010, gd, ge)
new_esEs2(@3(yu310, yu311, yu312), @3(yu40010, yu40011, yu40012), he, app(ty_Maybe, bca), bbb) → new_esEs3(yu311, yu40011, bca)
new_esEs(@2(yu310, yu311), @2(yu40010, yu40011), app(ty_Maybe, de), ce) → new_esEs3(yu310, yu40010, de)
new_esEs(@2(yu310, yu311), @2(yu40010, yu40011), app(ty_[], da), ce) → new_esEs1(yu310, yu40010, da)
new_esEs3(Just(yu310), Just(yu40010), app(app(ty_Either, bde), bdf)) → new_esEs0(yu310, yu40010, bde, bdf)
new_esEs2(@3(yu310, yu311, yu312), @3(yu40010, yu40011, yu40012), he, hf, app(ty_Maybe, bag)) → new_esEs3(yu312, yu40012, bag)
new_esEs2(@3(yu310, yu311, yu312), @3(yu40010, yu40011, yu40012), app(app(ty_Either, bcd), bce), hf, bbb) → new_esEs0(yu310, yu40010, bcd, bce)
new_esEs1(:(yu310, yu311), :(yu40010, yu40011), gc) → new_esEs1(yu311, yu40011, gc)
new_esEs2(@3(yu310, yu311, yu312), @3(yu40010, yu40011, yu40012), he, app(ty_[], bbe), bbb) → new_esEs1(yu311, yu40011, bbe)
new_esEs0(Left(yu310), Left(yu40010), app(ty_Maybe, eg), dh) → new_esEs3(yu310, yu40010, eg)
new_esEs1(:(yu310, yu311), :(yu40010, yu40011), app(ty_[], gh)) → new_esEs1(yu310, yu40010, gh)
new_esEs(@2(yu310, yu311), @2(yu40010, yu40011), ba, app(app(ty_Either, bd), be)) → new_esEs0(yu311, yu40011, bd, be)
new_esEs0(Left(yu310), Left(yu40010), app(app(app(ty_@3, ed), ee), ef), dh) → new_esEs2(yu310, yu40010, ed, ee, ef)
new_esEs0(Left(yu310), Left(yu40010), app(app(ty_Either, ea), eb), dh) → new_esEs0(yu310, yu40010, ea, eb)
new_esEs0(Left(yu310), Left(yu40010), app(app(ty_@2, df), dg), dh) → new_esEs(yu310, yu40010, df, dg)
new_esEs(@2(yu310, yu311), @2(yu40010, yu40011), ba, app(ty_Maybe, cb)) → new_esEs3(yu311, yu40011, cb)
new_esEs(@2(yu310, yu311), @2(yu40010, yu40011), app(app(ty_Either, cf), cg), ce) → new_esEs0(yu310, yu40010, cf, cg)
new_esEs(@2(yu310, yu311), @2(yu40010, yu40011), ba, app(app(app(ty_@3, bg), bh), ca)) → new_esEs2(yu311, yu40011, bg, bh, ca)
new_esEs0(Right(yu310), Right(yu40010), eh, app(app(ty_Either, fc), fd)) → new_esEs0(yu310, yu40010, fc, fd)
new_esEs(@2(yu310, yu311), @2(yu40010, yu40011), ba, app(ty_[], bf)) → new_esEs1(yu311, yu40011, bf)
new_esEs1(:(yu310, yu311), :(yu40010, yu40011), app(app(ty_Either, gf), gg)) → new_esEs0(yu310, yu40010, gf, gg)
new_esEs0(Right(yu310), Right(yu40010), eh, app(ty_[], ff)) → new_esEs1(yu310, yu40010, ff)
new_esEs0(Left(yu310), Left(yu40010), app(ty_[], ec), dh) → new_esEs1(yu310, yu40010, ec)
new_esEs2(@3(yu310, yu311, yu312), @3(yu40010, yu40011, yu40012), he, app(app(app(ty_@3, bbf), bbg), bbh), bbb) → new_esEs2(yu311, yu40011, bbf, bbg, bbh)
new_esEs0(Right(yu310), Right(yu40010), eh, app(app(app(ty_@3, fg), fh), ga)) → new_esEs2(yu310, yu40010, fg, fh, ga)
new_esEs3(Just(yu310), Just(yu40010), app(app(app(ty_@3, bdh), bea), beb)) → new_esEs2(yu310, yu40010, bdh, bea, beb)
new_esEs3(Just(yu310), Just(yu40010), app(ty_Maybe, bec)) → new_esEs3(yu310, yu40010, bec)
new_esEs2(@3(yu310, yu311, yu312), @3(yu40010, yu40011, yu40012), app(ty_Maybe, bdb), hf, bbb) → new_esEs3(yu310, yu40010, bdb)
new_esEs3(Just(yu310), Just(yu40010), app(app(ty_@2, bdc), bdd)) → new_esEs(yu310, yu40010, bdc, bdd)
new_esEs0(Right(yu310), Right(yu40010), eh, app(ty_Maybe, gb)) → new_esEs3(yu310, yu40010, gb)
new_esEs(@2(yu310, yu311), @2(yu40010, yu40011), ba, app(app(ty_@2, bb), bc)) → new_esEs(yu311, yu40011, bb, bc)
new_esEs(@2(yu310, yu311), @2(yu40010, yu40011), app(app(app(ty_@3, db), dc), dd), ce) → new_esEs2(yu310, yu40010, db, dc, dd)
new_esEs2(@3(yu310, yu311, yu312), @3(yu40010, yu40011, yu40012), he, hf, app(ty_[], bac)) → new_esEs1(yu312, yu40012, bac)
new_esEs2(@3(yu310, yu311, yu312), @3(yu40010, yu40011, yu40012), he, app(app(ty_@2, bah), bba), bbb) → new_esEs(yu311, yu40011, bah, bba)
new_esEs3(Just(yu310), Just(yu40010), app(ty_[], bdg)) → new_esEs1(yu310, yu40010, bdg)
new_esEs2(@3(yu310, yu311, yu312), @3(yu40010, yu40011, yu40012), app(app(ty_@2, bcb), bcc), hf, bbb) → new_esEs(yu310, yu40010, bcb, bcc)
new_esEs2(@3(yu310, yu311, yu312), @3(yu40010, yu40011, yu40012), he, app(app(ty_Either, bbc), bbd), bbb) → new_esEs0(yu311, yu40011, bbc, bbd)
new_esEs0(Right(yu310), Right(yu40010), eh, app(app(ty_@2, fa), fb)) → new_esEs(yu310, yu40010, fa, fb)
new_esEs2(@3(yu310, yu311, yu312), @3(yu40010, yu40011, yu40012), he, hf, app(app(ty_@2, hg), hh)) → new_esEs(yu312, yu40012, hg, hh)
new_esEs2(@3(yu310, yu311, yu312), @3(yu40010, yu40011, yu40012), app(ty_[], bcf), hf, bbb) → new_esEs1(yu310, yu40010, bcf)
new_esEs1(:(yu310, yu311), :(yu40010, yu40011), app(app(app(ty_@3, ha), hb), hc)) → new_esEs2(yu310, yu40010, ha, hb, hc)
new_esEs1(:(yu310, yu311), :(yu40010, yu40011), app(ty_Maybe, hd)) → new_esEs3(yu310, yu40010, hd)
new_esEs2(@3(yu310, yu311, yu312), @3(yu40010, yu40011, yu40012), he, hf, app(app(ty_Either, baa), bab)) → new_esEs0(yu312, yu40012, baa, bab)
new_esEs2(@3(yu310, yu311, yu312), @3(yu40010, yu40011, yu40012), he, hf, app(app(app(ty_@3, bad), bae), baf)) → new_esEs2(yu312, yu40012, bad, bae, baf)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
QDP
                ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

new_lookup1(yu28, yu29, yu30, yu31, yu32, yu33, False, ba, bb, bc) → new_lookup(@2(yu28, yu29), yu33, ba, bb, bc)
new_lookup(@2(yu30, yu31), :(@2(@2(yu4000, yu4001), yu401), yu41), bd, be, bf) → new_lookup1(yu30, yu31, yu4000, yu4001, yu401, yu41, new_asAs(new_esEs5(yu30, yu4000, be), new_esEs4(yu31, yu4001, bf)), bd, be, bf)

The TRS R consists of the following rules:

new_esEs23(yu310, yu40010, ty_@0) → new_esEs20(yu310, yu40010)
new_esEs23(yu310, yu40010, app(app(ty_Either, hc), hd)) → new_esEs12(yu310, yu40010, hc, hd)
new_esEs12(Right(yu310), Right(yu40010), de, app(app(app(ty_@3, bhb), bhc), bhd)) → new_esEs15(yu310, yu40010, bhb, bhc, bhd)
new_primPlusNat1(Succ(yu4800), Succ(yu40011000)) → Succ(Succ(new_primPlusNat1(yu4800, yu40011000)))
new_primEqInt(Neg(Succ(yu3100)), Pos(yu40010)) → False
new_primEqInt(Pos(Succ(yu3100)), Neg(yu40010)) → False
new_esEs26(yu311, yu40011, app(app(ty_Either, bda), bdb)) → new_esEs12(yu311, yu40011, bda, bdb)
new_esEs12(Right(yu310), Right(yu40010), de, ty_Double) → new_esEs14(yu310, yu40010)
new_esEs22(yu311, yu40011, ty_@0) → new_esEs20(yu311, yu40011)
new_esEs22(yu311, yu40011, app(ty_[], gc)) → new_esEs6(yu311, yu40011, gc)
new_esEs12(Right(yu310), Right(yu40010), de, ty_Integer) → new_esEs17(yu310, yu40010)
new_esEs26(yu311, yu40011, app(ty_Ratio, bdg)) → new_esEs16(yu311, yu40011, bdg)
new_esEs7(yu310, yu40010, ty_Integer) → new_esEs17(yu310, yu40010)
new_esEs26(yu311, yu40011, ty_Double) → new_esEs14(yu311, yu40011)
new_esEs12(Right(yu310), Right(yu40010), de, app(ty_Ratio, bhe)) → new_esEs16(yu310, yu40010, bhe)
new_esEs19(Just(yu310), Just(yu40010), ty_Char) → new_esEs9(yu310, yu40010)
new_primEqInt(Neg(Zero), Pos(Succ(yu400100))) → False
new_esEs6(:(yu310, yu311), :(yu40010, yu40011), bg) → new_asAs(new_esEs7(yu310, yu40010, bg), new_esEs6(yu311, yu40011, bg))
new_primEqInt(Pos(Zero), Neg(Succ(yu400100))) → False
new_esEs4(yu31, yu4001, ty_Int) → new_esEs18(yu31, yu4001)
new_esEs12(Left(yu310), Left(yu40010), app(ty_Ratio, bgc), df) → new_esEs16(yu310, yu40010, bgc)
new_esEs7(yu310, yu40010, ty_Float) → new_esEs11(yu310, yu40010)
new_esEs26(yu311, yu40011, app(ty_Maybe, bdh)) → new_esEs19(yu311, yu40011, bdh)
new_esEs23(yu310, yu40010, ty_Int) → new_esEs18(yu310, yu40010)
new_esEs21(yu312, yu40012, app(ty_Maybe, ff)) → new_esEs19(yu312, yu40012, ff)
new_primMulNat0(Zero, Zero) → Zero
new_esEs27(yu310, yu40010, app(ty_Ratio, bfa)) → new_esEs16(yu310, yu40010, bfa)
new_esEs19(Just(yu310), Just(yu40010), app(app(ty_Either, bbg), bbh)) → new_esEs12(yu310, yu40010, bbg, bbh)
new_esEs12(Left(yu310), Left(yu40010), ty_@0, df) → new_esEs20(yu310, yu40010)
new_esEs12(Right(yu310), Right(yu40010), de, ty_Int) → new_esEs18(yu310, yu40010)
new_esEs23(yu310, yu40010, ty_Float) → new_esEs11(yu310, yu40010)
new_esEs22(yu311, yu40011, ty_Char) → new_esEs9(yu311, yu40011)
new_esEs21(yu312, yu40012, app(app(ty_Either, ef), eg)) → new_esEs12(yu312, yu40012, ef, eg)
new_primPlusNat0(Zero, yu4001100) → Succ(yu4001100)
new_esEs22(yu311, yu40011, ty_Float) → new_esEs11(yu311, yu40011)
new_esEs21(yu312, yu40012, ty_@0) → new_esEs20(yu312, yu40012)
new_esEs19(Just(yu310), Just(yu40010), ty_Ordering) → new_esEs13(yu310, yu40010)
new_esEs13(EQ, EQ) → True
new_esEs26(yu311, yu40011, ty_Int) → new_esEs18(yu311, yu40011)
new_esEs5(yu30, yu4000, ty_Float) → new_esEs11(yu30, yu4000)
new_esEs19(Just(yu310), Just(yu40010), ty_@0) → new_esEs20(yu310, yu40010)
new_sr(Neg(yu3110), Pos(yu400110)) → Neg(new_primMulNat0(yu3110, yu400110))
new_sr(Pos(yu3110), Neg(yu400110)) → Neg(new_primMulNat0(yu3110, yu400110))
new_esEs27(yu310, yu40010, app(app(ty_@2, bea), beb)) → new_esEs8(yu310, yu40010, bea, beb)
new_esEs23(yu310, yu40010, app(ty_Maybe, bab)) → new_esEs19(yu310, yu40010, bab)
new_esEs19(Just(yu310), Just(yu40010), ty_Bool) → new_esEs10(yu310, yu40010)
new_esEs5(yu30, yu4000, app(app(ty_Either, bae), baf)) → new_esEs12(yu30, yu4000, bae, baf)
new_esEs22(yu311, yu40011, ty_Bool) → new_esEs10(yu311, yu40011)
new_esEs4(yu31, yu4001, ty_@0) → new_esEs20(yu31, yu4001)
new_esEs5(yu30, yu4000, app(ty_Ratio, bbc)) → new_esEs16(yu30, yu4000, bbc)
new_esEs12(Left(yu310), Right(yu40010), de, df) → False
new_esEs12(Right(yu310), Left(yu40010), de, df) → False
new_esEs12(Left(yu310), Left(yu40010), app(app(ty_@2, bfc), bfd), df) → new_esEs8(yu310, yu40010, bfc, bfd)
new_esEs19(Just(yu310), Nothing, ec) → False
new_esEs19(Nothing, Just(yu40010), ec) → False
new_esEs4(yu31, yu4001, ty_Float) → new_esEs11(yu31, yu4001)
new_esEs27(yu310, yu40010, ty_Bool) → new_esEs10(yu310, yu40010)
new_esEs7(yu310, yu40010, app(app(ty_Either, cb), cc)) → new_esEs12(yu310, yu40010, cb, cc)
new_esEs25(yu310, yu40010, ty_Integer) → new_esEs17(yu310, yu40010)
new_esEs19(Nothing, Nothing, ec) → True
new_esEs27(yu310, yu40010, app(app(ty_Either, bec), bed)) → new_esEs12(yu310, yu40010, bec, bed)
new_esEs10(True, True) → True
new_esEs7(yu310, yu40010, ty_Int) → new_esEs18(yu310, yu40010)
new_esEs13(GT, GT) → True
new_esEs12(Right(yu310), Right(yu40010), de, ty_Bool) → new_esEs10(yu310, yu40010)
new_esEs27(yu310, yu40010, ty_Double) → new_esEs14(yu310, yu40010)
new_esEs19(Just(yu310), Just(yu40010), app(app(ty_@2, bbe), bbf)) → new_esEs8(yu310, yu40010, bbe, bbf)
new_esEs12(Left(yu310), Left(yu40010), app(app(ty_Either, bfe), bff), df) → new_esEs12(yu310, yu40010, bfe, bff)
new_esEs12(Left(yu310), Left(yu40010), app(ty_Maybe, bgd), df) → new_esEs19(yu310, yu40010, bgd)
new_primEqNat0(Zero, Succ(yu400100)) → False
new_primEqNat0(Succ(yu3100), Zero) → False
new_esEs17(Integer(yu310), Integer(yu40010)) → new_primEqInt(yu310, yu40010)
new_esEs5(yu30, yu4000, app(ty_[], bag)) → new_esEs6(yu30, yu4000, bag)
new_esEs21(yu312, yu40012, app(app(ty_@2, ed), ee)) → new_esEs8(yu312, yu40012, ed, ee)
new_esEs12(Right(yu310), Right(yu40010), de, app(ty_Maybe, bhf)) → new_esEs19(yu310, yu40010, bhf)
new_primEqInt(Pos(Zero), Pos(Zero)) → True
new_esEs22(yu311, yu40011, ty_Double) → new_esEs14(yu311, yu40011)
new_esEs26(yu311, yu40011, ty_Bool) → new_esEs10(yu311, yu40011)
new_esEs13(EQ, LT) → False
new_esEs13(LT, EQ) → False
new_esEs27(yu310, yu40010, ty_Int) → new_esEs18(yu310, yu40010)
new_esEs26(yu311, yu40011, app(app(ty_@2, bcg), bch)) → new_esEs8(yu311, yu40011, bcg, bch)
new_esEs27(yu310, yu40010, ty_Float) → new_esEs11(yu310, yu40010)
new_esEs20(@0, @0) → True
new_esEs22(yu311, yu40011, ty_Ordering) → new_esEs13(yu311, yu40011)
new_esEs5(yu30, yu4000, ty_Ordering) → new_esEs13(yu30, yu4000)
new_esEs21(yu312, yu40012, ty_Ordering) → new_esEs13(yu312, yu40012)
new_esEs15(@3(yu310, yu311, yu312), @3(yu40010, yu40011, yu40012), dg, dh, ea) → new_asAs(new_esEs23(yu310, yu40010, dg), new_asAs(new_esEs22(yu311, yu40011, dh), new_esEs21(yu312, yu40012, ea)))
new_esEs12(Left(yu310), Left(yu40010), ty_Bool, df) → new_esEs10(yu310, yu40010)
new_esEs4(yu31, yu4001, ty_Char) → new_esEs9(yu31, yu4001)
new_esEs5(yu30, yu4000, ty_@0) → new_esEs20(yu30, yu4000)
new_esEs4(yu31, yu4001, ty_Double) → new_esEs14(yu31, yu4001)
new_esEs4(yu31, yu4001, app(app(app(ty_@3, dg), dh), ea)) → new_esEs15(yu31, yu4001, dg, dh, ea)
new_esEs21(yu312, yu40012, ty_Int) → new_esEs18(yu312, yu40012)
new_esEs23(yu310, yu40010, app(app(ty_@2, ha), hb)) → new_esEs8(yu310, yu40010, ha, hb)
new_esEs18(yu31, yu4001) → new_primEqInt(yu31, yu4001)
new_esEs6([], :(yu40010, yu40011), bg) → False
new_esEs6(:(yu310, yu311), [], bg) → False
new_esEs7(yu310, yu40010, app(ty_Maybe, db)) → new_esEs19(yu310, yu40010, db)
new_esEs23(yu310, yu40010, ty_Double) → new_esEs14(yu310, yu40010)
new_esEs7(yu310, yu40010, app(ty_[], cd)) → new_esEs6(yu310, yu40010, cd)
new_esEs19(Just(yu310), Just(yu40010), app(ty_[], bca)) → new_esEs6(yu310, yu40010, bca)
new_esEs21(yu312, yu40012, ty_Char) → new_esEs9(yu312, yu40012)
new_esEs23(yu310, yu40010, app(ty_Ratio, baa)) → new_esEs16(yu310, yu40010, baa)
new_esEs19(Just(yu310), Just(yu40010), app(app(app(ty_@3, bcb), bcc), bcd)) → new_esEs15(yu310, yu40010, bcb, bcc, bcd)
new_esEs22(yu311, yu40011, app(ty_Ratio, gg)) → new_esEs16(yu311, yu40011, gg)
new_esEs8(@2(yu310, yu311), @2(yu40010, yu40011), dc, dd) → new_asAs(new_esEs27(yu310, yu40010, dc), new_esEs26(yu311, yu40011, dd))
new_esEs7(yu310, yu40010, ty_Ordering) → new_esEs13(yu310, yu40010)
new_esEs21(yu312, yu40012, ty_Integer) → new_esEs17(yu312, yu40012)
new_esEs22(yu311, yu40011, app(app(app(ty_@3, gd), ge), gf)) → new_esEs15(yu311, yu40011, gd, ge, gf)
new_esEs4(yu31, yu4001, app(ty_[], bg)) → new_esEs6(yu31, yu4001, bg)
new_esEs26(yu311, yu40011, app(ty_[], bdc)) → new_esEs6(yu311, yu40011, bdc)
new_sr(Neg(yu3110), Neg(yu400110)) → Pos(new_primMulNat0(yu3110, yu400110))
new_esEs27(yu310, yu40010, ty_Ordering) → new_esEs13(yu310, yu40010)
new_esEs12(Left(yu310), Left(yu40010), ty_Char, df) → new_esEs9(yu310, yu40010)
new_sr(Pos(yu3110), Pos(yu400110)) → Pos(new_primMulNat0(yu3110, yu400110))
new_asAs(False, yu47) → False
new_esEs22(yu311, yu40011, ty_Int) → new_esEs18(yu311, yu40011)
new_primEqNat0(Zero, Zero) → True
new_esEs22(yu311, yu40011, app(app(ty_Either, ga), gb)) → new_esEs12(yu311, yu40011, ga, gb)
new_primMulNat0(Zero, Succ(yu4001100)) → Zero
new_primMulNat0(Succ(yu31100), Zero) → Zero
new_esEs13(GT, EQ) → False
new_esEs13(EQ, GT) → False
new_esEs4(yu31, yu4001, ty_Bool) → new_esEs10(yu31, yu4001)
new_esEs12(Right(yu310), Right(yu40010), de, ty_Float) → new_esEs11(yu310, yu40010)
new_esEs13(GT, LT) → False
new_esEs13(LT, GT) → False
new_esEs19(Just(yu310), Just(yu40010), ty_Float) → new_esEs11(yu310, yu40010)
new_esEs14(Double(yu310, yu311), Double(yu40010, yu40011)) → new_esEs18(new_sr(yu310, yu40010), new_sr(yu311, yu40011))
new_esEs19(Just(yu310), Just(yu40010), ty_Integer) → new_esEs17(yu310, yu40010)
new_esEs5(yu30, yu4000, app(app(app(ty_@3, bah), bba), bbb)) → new_esEs15(yu30, yu4000, bah, bba, bbb)
new_esEs12(Left(yu310), Left(yu40010), ty_Integer, df) → new_esEs17(yu310, yu40010)
new_esEs24(yu311, yu40011, ty_Integer) → new_esEs17(yu311, yu40011)
new_esEs4(yu31, yu4001, ty_Integer) → new_esEs17(yu31, yu4001)
new_esEs12(Left(yu310), Left(yu40010), ty_Float, df) → new_esEs11(yu310, yu40010)
new_esEs16(:%(yu310, yu311), :%(yu40010, yu40011), eb) → new_asAs(new_esEs25(yu310, yu40010, eb), new_esEs24(yu311, yu40011, eb))
new_esEs7(yu310, yu40010, ty_Bool) → new_esEs10(yu310, yu40010)
new_esEs23(yu310, yu40010, ty_Char) → new_esEs9(yu310, yu40010)
new_esEs7(yu310, yu40010, app(app(ty_@2, bh), ca)) → new_esEs8(yu310, yu40010, bh, ca)
new_esEs5(yu30, yu4000, ty_Char) → new_esEs9(yu30, yu4000)
new_esEs27(yu310, yu40010, ty_@0) → new_esEs20(yu310, yu40010)
new_primPlusNat0(Succ(yu480), yu4001100) → Succ(Succ(new_primPlusNat1(yu480, yu4001100)))
new_esEs7(yu310, yu40010, ty_Double) → new_esEs14(yu310, yu40010)
new_esEs23(yu310, yu40010, ty_Bool) → new_esEs10(yu310, yu40010)
new_esEs12(Right(yu310), Right(yu40010), de, app(ty_[], bha)) → new_esEs6(yu310, yu40010, bha)
new_esEs26(yu311, yu40011, ty_Float) → new_esEs11(yu311, yu40011)
new_esEs21(yu312, yu40012, app(ty_Ratio, fd)) → new_esEs16(yu312, yu40012, fd)
new_esEs12(Left(yu310), Left(yu40010), ty_Int, df) → new_esEs18(yu310, yu40010)
new_esEs4(yu31, yu4001, app(app(ty_Either, de), df)) → new_esEs12(yu31, yu4001, de, df)
new_primEqInt(Neg(Succ(yu3100)), Neg(Succ(yu400100))) → new_primEqNat0(yu3100, yu400100)
new_esEs22(yu311, yu40011, app(ty_Maybe, gh)) → new_esEs19(yu311, yu40011, gh)
new_esEs23(yu310, yu40010, app(ty_[], he)) → new_esEs6(yu310, yu40010, he)
new_esEs6([], [], bg) → True
new_esEs12(Left(yu310), Left(yu40010), ty_Double, df) → new_esEs14(yu310, yu40010)
new_primPlusNat1(Zero, Succ(yu40011000)) → Succ(yu40011000)
new_primPlusNat1(Succ(yu4800), Zero) → Succ(yu4800)
new_esEs23(yu310, yu40010, app(app(app(ty_@3, hf), hg), hh)) → new_esEs15(yu310, yu40010, hf, hg, hh)
new_esEs19(Just(yu310), Just(yu40010), ty_Int) → new_esEs18(yu310, yu40010)
new_esEs5(yu30, yu4000, ty_Int) → new_esEs18(yu30, yu4000)
new_esEs26(yu311, yu40011, app(app(app(ty_@3, bdd), bde), bdf)) → new_esEs15(yu311, yu40011, bdd, bde, bdf)
new_esEs4(yu31, yu4001, ty_Ordering) → new_esEs13(yu31, yu4001)
new_esEs25(yu310, yu40010, ty_Int) → new_esEs18(yu310, yu40010)
new_esEs21(yu312, yu40012, ty_Double) → new_esEs14(yu312, yu40012)
new_primEqInt(Neg(Zero), Neg(Zero)) → True
new_esEs12(Right(yu310), Right(yu40010), de, app(app(ty_Either, bgg), bgh)) → new_esEs12(yu310, yu40010, bgg, bgh)
new_esEs12(Right(yu310), Right(yu40010), de, ty_@0) → new_esEs20(yu310, yu40010)
new_esEs22(yu311, yu40011, ty_Integer) → new_esEs17(yu311, yu40011)
new_esEs4(yu31, yu4001, app(app(ty_@2, dc), dd)) → new_esEs8(yu31, yu4001, dc, dd)
new_esEs19(Just(yu310), Just(yu40010), ty_Double) → new_esEs14(yu310, yu40010)
new_primEqInt(Neg(Zero), Neg(Succ(yu400100))) → False
new_primEqInt(Neg(Succ(yu3100)), Neg(Zero)) → False
new_esEs21(yu312, yu40012, app(ty_[], eh)) → new_esEs6(yu312, yu40012, eh)
new_esEs12(Right(yu310), Right(yu40010), de, ty_Ordering) → new_esEs13(yu310, yu40010)
new_esEs26(yu311, yu40011, ty_Char) → new_esEs9(yu311, yu40011)
new_esEs21(yu312, yu40012, ty_Float) → new_esEs11(yu312, yu40012)
new_esEs5(yu30, yu4000, ty_Double) → new_esEs14(yu30, yu4000)
new_esEs19(Just(yu310), Just(yu40010), app(ty_Maybe, bcf)) → new_esEs19(yu310, yu40010, bcf)
new_esEs9(Char(yu310), Char(yu40010)) → new_primEqNat0(yu310, yu40010)
new_esEs23(yu310, yu40010, ty_Integer) → new_esEs17(yu310, yu40010)
new_esEs10(False, False) → True
new_esEs5(yu30, yu4000, app(app(ty_@2, bac), bad)) → new_esEs8(yu30, yu4000, bac, bad)
new_primPlusNat1(Zero, Zero) → Zero
new_esEs7(yu310, yu40010, ty_Char) → new_esEs9(yu310, yu40010)
new_esEs5(yu30, yu4000, ty_Integer) → new_esEs17(yu30, yu4000)
new_esEs21(yu312, yu40012, app(app(app(ty_@3, fa), fb), fc)) → new_esEs15(yu312, yu40012, fa, fb, fc)
new_esEs27(yu310, yu40010, app(ty_[], bee)) → new_esEs6(yu310, yu40010, bee)
new_asAs(True, yu47) → yu47
new_esEs7(yu310, yu40010, ty_@0) → new_esEs20(yu310, yu40010)
new_primMulNat0(Succ(yu31100), Succ(yu4001100)) → new_primPlusNat0(new_primMulNat0(yu31100, Succ(yu4001100)), yu4001100)
new_esEs12(Right(yu310), Right(yu40010), de, app(app(ty_@2, bge), bgf)) → new_esEs8(yu310, yu40010, bge, bgf)
new_esEs22(yu311, yu40011, app(app(ty_@2, fg), fh)) → new_esEs8(yu311, yu40011, fg, fh)
new_esEs10(True, False) → False
new_esEs10(False, True) → False
new_esEs26(yu311, yu40011, ty_Integer) → new_esEs17(yu311, yu40011)
new_esEs13(LT, LT) → True
new_primEqInt(Pos(Succ(yu3100)), Pos(Succ(yu400100))) → new_primEqNat0(yu3100, yu400100)
new_esEs19(Just(yu310), Just(yu40010), app(ty_Ratio, bce)) → new_esEs16(yu310, yu40010, bce)
new_esEs5(yu30, yu4000, ty_Bool) → new_esEs10(yu30, yu4000)
new_esEs4(yu31, yu4001, app(ty_Maybe, ec)) → new_esEs19(yu31, yu4001, ec)
new_esEs11(Float(yu310, yu311), Float(yu40010, yu40011)) → new_esEs18(new_sr(yu310, yu40010), new_sr(yu311, yu40011))
new_esEs7(yu310, yu40010, app(app(app(ty_@3, ce), cf), cg)) → new_esEs15(yu310, yu40010, ce, cf, cg)
new_esEs27(yu310, yu40010, app(ty_Maybe, bfb)) → new_esEs19(yu310, yu40010, bfb)
new_esEs27(yu310, yu40010, app(app(app(ty_@3, bef), beg), beh)) → new_esEs15(yu310, yu40010, bef, beg, beh)
new_esEs12(Left(yu310), Left(yu40010), app(ty_[], bfg), df) → new_esEs6(yu310, yu40010, bfg)
new_esEs24(yu311, yu40011, ty_Int) → new_esEs18(yu311, yu40011)
new_primEqNat0(Succ(yu3100), Succ(yu400100)) → new_primEqNat0(yu3100, yu400100)
new_esEs5(yu30, yu4000, app(ty_Maybe, bbd)) → new_esEs19(yu30, yu4000, bbd)
new_esEs27(yu310, yu40010, ty_Integer) → new_esEs17(yu310, yu40010)
new_esEs26(yu311, yu40011, ty_@0) → new_esEs20(yu311, yu40011)
new_esEs21(yu312, yu40012, ty_Bool) → new_esEs10(yu312, yu40012)
new_esEs12(Left(yu310), Left(yu40010), ty_Ordering, df) → new_esEs13(yu310, yu40010)
new_esEs7(yu310, yu40010, app(ty_Ratio, da)) → new_esEs16(yu310, yu40010, da)
new_esEs4(yu31, yu4001, app(ty_Ratio, eb)) → new_esEs16(yu31, yu4001, eb)
new_esEs26(yu311, yu40011, ty_Ordering) → new_esEs13(yu311, yu40011)
new_primEqInt(Pos(Succ(yu3100)), Pos(Zero)) → False
new_primEqInt(Pos(Zero), Pos(Succ(yu400100))) → False
new_esEs12(Left(yu310), Left(yu40010), app(app(app(ty_@3, bfh), bga), bgb), df) → new_esEs15(yu310, yu40010, bfh, bga, bgb)
new_primEqInt(Neg(Zero), Pos(Zero)) → True
new_primEqInt(Pos(Zero), Neg(Zero)) → True
new_esEs12(Right(yu310), Right(yu40010), de, ty_Char) → new_esEs9(yu310, yu40010)
new_esEs27(yu310, yu40010, ty_Char) → new_esEs9(yu310, yu40010)
new_esEs23(yu310, yu40010, ty_Ordering) → new_esEs13(yu310, yu40010)

The set Q consists of the following terms:

new_esEs9(Char(x0), Char(x1))
new_esEs25(x0, x1, ty_Int)
new_esEs6(:(x0, x1), [], x2)
new_esEs19(Just(x0), Just(x1), ty_Ordering)
new_esEs4(x0, x1, ty_Integer)
new_esEs23(x0, x1, app(ty_[], x2))
new_primEqInt(Neg(Succ(x0)), Neg(Zero))
new_esEs27(x0, x1, ty_Char)
new_sr(Neg(x0), Neg(x1))
new_esEs7(x0, x1, ty_Bool)
new_primEqInt(Pos(Succ(x0)), Pos(Succ(x1)))
new_esEs26(x0, x1, ty_Char)
new_esEs21(x0, x1, ty_Ordering)
new_esEs5(x0, x1, ty_Char)
new_esEs5(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs26(x0, x1, ty_Ordering)
new_esEs27(x0, x1, ty_Integer)
new_primEqInt(Neg(Zero), Pos(Zero))
new_primEqInt(Pos(Zero), Neg(Zero))
new_primEqNat0(Succ(x0), Zero)
new_esEs12(Right(x0), Right(x1), x2, app(app(ty_Either, x3), x4))
new_esEs21(x0, x1, app(ty_[], x2))
new_esEs23(x0, x1, app(app(ty_Either, x2), x3))
new_esEs5(x0, x1, ty_Float)
new_esEs12(Left(x0), Left(x1), ty_Char, x2)
new_esEs12(Left(x0), Left(x1), ty_Integer, x2)
new_esEs27(x0, x1, ty_Int)
new_primEqInt(Pos(Succ(x0)), Pos(Zero))
new_asAs(True, x0)
new_esEs13(GT, GT)
new_esEs27(x0, x1, ty_Ordering)
new_esEs21(x0, x1, app(app(ty_Either, x2), x3))
new_esEs5(x0, x1, ty_Bool)
new_esEs6([], [], x0)
new_esEs26(x0, x1, ty_@0)
new_primEqInt(Neg(Zero), Neg(Zero))
new_esEs23(x0, x1, ty_Ordering)
new_esEs19(Just(x0), Just(x1), ty_Int)
new_esEs24(x0, x1, ty_Integer)
new_esEs22(x0, x1, ty_Double)
new_esEs22(x0, x1, app(ty_Ratio, x2))
new_esEs26(x0, x1, ty_Bool)
new_esEs25(x0, x1, ty_Integer)
new_esEs4(x0, x1, app(ty_Ratio, x2))
new_esEs24(x0, x1, ty_Int)
new_esEs21(x0, x1, ty_Float)
new_esEs22(x0, x1, ty_@0)
new_esEs4(x0, x1, ty_Float)
new_primEqInt(Neg(Succ(x0)), Neg(Succ(x1)))
new_esEs27(x0, x1, app(ty_Maybe, x2))
new_esEs12(Right(x0), Right(x1), x2, app(ty_Ratio, x3))
new_primEqNat0(Succ(x0), Succ(x1))
new_esEs6([], :(x0, x1), x2)
new_esEs7(x0, x1, app(app(ty_@2, x2), x3))
new_esEs7(x0, x1, app(app(ty_Either, x2), x3))
new_esEs7(x0, x1, ty_Int)
new_esEs12(Right(x0), Right(x1), x2, ty_Int)
new_esEs19(Just(x0), Just(x1), app(ty_Ratio, x2))
new_esEs12(Right(x0), Right(x1), x2, ty_Float)
new_esEs16(:%(x0, x1), :%(x2, x3), x4)
new_esEs26(x0, x1, ty_Float)
new_esEs5(x0, x1, ty_@0)
new_esEs22(x0, x1, app(app(ty_@2, x2), x3))
new_esEs21(x0, x1, ty_Double)
new_primEqInt(Pos(Succ(x0)), Neg(x1))
new_primEqInt(Neg(Succ(x0)), Pos(x1))
new_esEs22(x0, x1, ty_Char)
new_esEs19(Just(x0), Just(x1), app(app(ty_@2, x2), x3))
new_esEs7(x0, x1, ty_Double)
new_esEs19(Nothing, Just(x0), x1)
new_esEs27(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_primPlusNat1(Zero, Succ(x0))
new_esEs22(x0, x1, app(ty_[], x2))
new_esEs23(x0, x1, ty_Float)
new_esEs5(x0, x1, ty_Double)
new_esEs22(x0, x1, app(app(ty_Either, x2), x3))
new_esEs6(:(x0, x1), :(x2, x3), x4)
new_primMulNat0(Succ(x0), Zero)
new_esEs7(x0, x1, ty_Ordering)
new_primEqInt(Pos(Zero), Pos(Succ(x0)))
new_esEs26(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs27(x0, x1, app(ty_[], x2))
new_esEs15(@3(x0, x1, x2), @3(x3, x4, x5), x6, x7, x8)
new_esEs5(x0, x1, ty_Ordering)
new_esEs21(x0, x1, ty_Bool)
new_esEs26(x0, x1, ty_Int)
new_primMulNat0(Zero, Succ(x0))
new_esEs13(LT, GT)
new_esEs13(GT, LT)
new_esEs12(Right(x0), Right(x1), x2, app(app(app(ty_@3, x3), x4), x5))
new_esEs21(x0, x1, app(ty_Ratio, x2))
new_esEs4(x0, x1, app(app(ty_Either, x2), x3))
new_esEs10(False, False)
new_esEs4(x0, x1, ty_Bool)
new_esEs5(x0, x1, app(ty_Ratio, x2))
new_esEs27(x0, x1, app(ty_Ratio, x2))
new_esEs7(x0, x1, app(ty_[], x2))
new_primEqNat0(Zero, Zero)
new_esEs26(x0, x1, app(app(ty_@2, x2), x3))
new_esEs5(x0, x1, app(ty_[], x2))
new_esEs27(x0, x1, ty_Double)
new_esEs12(Right(x0), Right(x1), x2, ty_Bool)
new_esEs21(x0, x1, ty_Int)
new_esEs4(x0, x1, ty_Char)
new_esEs12(Right(x0), Right(x1), x2, app(app(ty_@2, x3), x4))
new_esEs8(@2(x0, x1), @2(x2, x3), x4, x5)
new_esEs26(x0, x1, ty_Double)
new_esEs12(Left(x0), Left(x1), ty_Float, x2)
new_esEs7(x0, x1, app(ty_Ratio, x2))
new_esEs13(EQ, GT)
new_esEs13(GT, EQ)
new_esEs4(x0, x1, ty_Int)
new_esEs13(LT, LT)
new_esEs11(Float(x0, x1), Float(x2, x3))
new_esEs12(Right(x0), Right(x1), x2, ty_Double)
new_esEs12(Left(x0), Left(x1), app(ty_Maybe, x2), x3)
new_primPlusNat0(Succ(x0), x1)
new_esEs22(x0, x1, app(ty_Maybe, x2))
new_primMulNat0(Zero, Zero)
new_esEs12(Left(x0), Left(x1), ty_Ordering, x2)
new_esEs21(x0, x1, ty_Char)
new_esEs12(Left(x0), Left(x1), app(app(ty_@2, x2), x3), x4)
new_esEs10(True, False)
new_esEs10(False, True)
new_esEs12(Left(x0), Left(x1), app(app(app(ty_@3, x2), x3), x4), x5)
new_esEs23(x0, x1, ty_@0)
new_primPlusNat1(Succ(x0), Succ(x1))
new_esEs19(Just(x0), Just(x1), ty_@0)
new_esEs5(x0, x1, ty_Integer)
new_primEqNat0(Zero, Succ(x0))
new_esEs5(x0, x1, app(app(ty_@2, x2), x3))
new_esEs12(Left(x0), Left(x1), ty_Int, x2)
new_esEs7(x0, x1, ty_Float)
new_esEs7(x0, x1, ty_Integer)
new_esEs5(x0, x1, ty_Int)
new_esEs12(Left(x0), Left(x1), ty_Double, x2)
new_esEs22(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_sr(Pos(x0), Neg(x1))
new_sr(Neg(x0), Pos(x1))
new_esEs12(Right(x0), Right(x1), x2, ty_Ordering)
new_esEs21(x0, x1, app(app(ty_@2, x2), x3))
new_esEs5(x0, x1, app(ty_Maybe, x2))
new_esEs22(x0, x1, ty_Integer)
new_esEs13(EQ, LT)
new_esEs13(LT, EQ)
new_esEs18(x0, x1)
new_esEs27(x0, x1, app(app(ty_@2, x2), x3))
new_esEs12(Left(x0), Right(x1), x2, x3)
new_esEs12(Right(x0), Left(x1), x2, x3)
new_esEs27(x0, x1, app(app(ty_Either, x2), x3))
new_esEs19(Just(x0), Just(x1), ty_Float)
new_esEs23(x0, x1, ty_Char)
new_sr(Pos(x0), Pos(x1))
new_esEs12(Right(x0), Right(x1), x2, ty_@0)
new_esEs13(EQ, EQ)
new_esEs12(Left(x0), Left(x1), ty_Bool, x2)
new_esEs22(x0, x1, ty_Float)
new_esEs7(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs19(Nothing, Nothing, x0)
new_esEs21(x0, x1, ty_Integer)
new_primMulNat0(Succ(x0), Succ(x1))
new_esEs12(Right(x0), Right(x1), x2, ty_Integer)
new_esEs12(Left(x0), Left(x1), ty_@0, x2)
new_esEs17(Integer(x0), Integer(x1))
new_esEs20(@0, @0)
new_esEs12(Left(x0), Left(x1), app(ty_[], x2), x3)
new_esEs4(x0, x1, ty_Ordering)
new_esEs4(x0, x1, ty_@0)
new_esEs27(x0, x1, ty_Bool)
new_esEs26(x0, x1, ty_Integer)
new_esEs22(x0, x1, ty_Bool)
new_esEs26(x0, x1, app(ty_[], x2))
new_esEs23(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs26(x0, x1, app(ty_Ratio, x2))
new_esEs19(Just(x0), Just(x1), ty_Integer)
new_esEs21(x0, x1, app(ty_Maybe, x2))
new_esEs23(x0, x1, app(app(ty_@2, x2), x3))
new_esEs19(Just(x0), Just(x1), app(ty_[], x2))
new_esEs22(x0, x1, ty_Int)
new_esEs27(x0, x1, ty_Float)
new_esEs12(Left(x0), Left(x1), app(ty_Ratio, x2), x3)
new_esEs21(x0, x1, ty_@0)
new_esEs7(x0, x1, app(ty_Maybe, x2))
new_esEs23(x0, x1, app(ty_Ratio, x2))
new_primPlusNat1(Zero, Zero)
new_esEs19(Just(x0), Just(x1), app(app(ty_Either, x2), x3))
new_asAs(False, x0)
new_esEs19(Just(x0), Just(x1), app(ty_Maybe, x2))
new_esEs10(True, True)
new_esEs4(x0, x1, ty_Double)
new_esEs19(Just(x0), Nothing, x1)
new_esEs19(Just(x0), Just(x1), app(app(app(ty_@3, x2), x3), x4))
new_primPlusNat0(Zero, x0)
new_esEs5(x0, x1, app(app(ty_Either, x2), x3))
new_esEs19(Just(x0), Just(x1), ty_Char)
new_esEs4(x0, x1, app(app(ty_@2, x2), x3))
new_primEqInt(Pos(Zero), Pos(Zero))
new_esEs26(x0, x1, app(app(ty_Either, x2), x3))
new_esEs4(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs23(x0, x1, ty_Double)
new_esEs21(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs23(x0, x1, ty_Int)
new_esEs23(x0, x1, ty_Bool)
new_esEs12(Right(x0), Right(x1), x2, app(ty_[], x3))
new_esEs27(x0, x1, ty_@0)
new_primPlusNat1(Succ(x0), Zero)
new_esEs22(x0, x1, ty_Ordering)
new_esEs12(Right(x0), Right(x1), x2, app(ty_Maybe, x3))
new_primEqInt(Neg(Zero), Neg(Succ(x0)))
new_primEqInt(Neg(Zero), Pos(Succ(x0)))
new_primEqInt(Pos(Zero), Neg(Succ(x0)))
new_esEs19(Just(x0), Just(x1), ty_Double)
new_esEs7(x0, x1, ty_@0)
new_esEs12(Left(x0), Left(x1), app(app(ty_Either, x2), x3), x4)
new_esEs14(Double(x0, x1), Double(x2, x3))
new_esEs12(Right(x0), Right(x1), x2, ty_Char)
new_esEs7(x0, x1, ty_Char)
new_esEs4(x0, x1, app(ty_[], x2))
new_esEs23(x0, x1, app(ty_Maybe, x2))
new_esEs19(Just(x0), Just(x1), ty_Bool)
new_esEs4(x0, x1, app(ty_Maybe, x2))
new_esEs23(x0, x1, ty_Integer)
new_esEs26(x0, x1, app(ty_Maybe, x2))

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: